COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE PREDCONST LIST 1[R←350]
C00005 ENDMK
C⊗;
DECLARE PREDCONST LIST 1[R←350];
DECLARE PREDCONST ELEMENT 1[R←350];

DECLARE INDVAR W W0 W1 W2 X X0 X1 X2 Y Y0 Y1 Y2 Z Z0 Z1 Z2;
DECLARE INDVAR u u0 u1 u2 v v0 v1 v2 w w0 w1 w2 ε LIST;
DECLARE INDCONST NILL ε LIST;
DECLARE INDVAR x x0 x1 x2 y y0 y1 y2 ε ELEMENT;

DECLARE OPCONST CONS 2;
DECLARE OPCONST CAR 1[R ← 600];
DECLARE OPCONST CDR 1[R ← 600];
DECLARE OPCONST cons(ELEMENT,LIST) = LIST;
DECLARE OPCONST car(LIST) = ELEMENT[R←600];
DECLARE OPCONST cdr(LIST) = LIST[R←600];

AXIOM CONS:
	∀X Y.(ELEMENT X ⊃ (LIST Y ⊃ LIST CONS(X,Y)))
;;

AXIOM CAR:
	∀X.(¬(X = NILL) ⊃ (LIST X ⊃ ELEMENT CAR X))
;;

AXIOM CDR:
	∀X.(¬X=NILL ⊃ (LIST X ⊃ LIST CDR X))
;;

AXIOM LIST:
	∀x u.(car cons(x,u) = x)
	∀x u.(cdr cons(x,u) = u)
	∀u.(¬u=NILL ⊃ u = cons(car u,cdr u))
;;

DECLARE PREDPAR P 1;

AXIOM INDUCTION:
	P(NILL) ∧ ∀u.(¬(u=NILL) ∧ P(cdr u) ⊃ P(u)) ⊃ ∀u.P(u)
	P(NILL) ∧ ∀X.(¬(X=NILL) ⊃ (LIST X ⊃ (P(CDR X) ⊃ P(X))))
		 ⊃ ∀X.(LIST X  ⊃ P(X))
;;

DECLARE OPCONST APP 2[L←400 R←395];

DECLARE OPCONST app(LIST,LIST) = LIST[L←400 R←395];

AXIOM APPEND:
	∀X Y.(X APP Y = IF X = NILL THEN Y ELSE CONS(CAR X, CDR X APP Y))
	∀u v.(u app v = IF ∃w.(u APP v = w) THEN u APP v ELSE NILL)
	∀u v.(u app v = IF LIST(u APP v) THEN u APP v ELSE NILL)
;;